(DEFPROP PRFFNS
 (PRFFNS PRFMAX PRFMIN RECTIFY COMMONTAIL COMMONHEAD)
VALUE)

(DEFPROP PRFMAX
 (LAMBDA(U PRMAX PRMIN ALPHA BETA)
  (COND
   ((NULL U) (LIST ALPHA PRMAX PRMIN))
   (T
    ((LAMBDA(S)
      (COND
       ((NOT (GREATERP (CAR S) ALPHA))
	(PRFMAX (CDR U)
		PRMAX
		(CONS (CONS (EXT (CAR U)) (CADDR S)) PRMIN)
		ALPHA
		BETA))
       ((LESSP (CAR S) BETA)
	(PRFMAX (CDR U)
		(CONS (EXT (CAR U)) (CADR S))
		(CONS (CONS (EXT (CAR U)) (CADDR S)) PRMIN)
		(CAR S)
		BETA))
       (T (LIST BETA (CONS (EXT (CAR U)) (CADR S)) NIL))))
     (COND
      ((TER (RECTIFY (CAR U)) ALPHA BETA)
       ((LAMBDA (V) (LIST V (LIST V) (LIST V)))
	(IMVAL (RECTIFY (CAR U)))))
      (T
       (PRFMIN (SUCCESSORS (RECTIFY (CAR U)))
	       NIL
	       (CONS BETA (QUOTE BETA-CUTOFF))
	       ALPHA
	       BETA)))))))
EXPR)

(DEFPROP PRFMIN
 (LAMBDA(U PRMAX PRMIN ALPHA BETA)
  (COND
   ((NULL U) (LIST BETA PRMAX PRMIN))
   (T
    ((LAMBDA(S)
      (COND
       ((NOT (GREATERP (CAR S) ALPHA))
	(LIST ALPHA NIL (CONS (EXT (CAR U)) (CADDR S))))
       ((LESSP (CAR S) BETA)
	(PRFMIN (CDR U)
		(CONS (CONS (EXT (CAR U)) (CADR S)) PRMAX)
		(CONS (EXT (CAR U)) (CADDR S))
		ALPHA
		(CAR S)))
       (T
	(PRFMIN (CDR U)
		(CONS (CONS (EXT (CAR U)) (CADR S)) PRMAX)
		PRMIN
		ALPHA
		BETA))))
     (COND
      ((TER (RECTIFY (CAR U)) ALPHA BETA)
       ((LAMBDA (V) (LIST V (LIST V) (LIST V)))
	(IMVAL (RECTIFY (CAR U)))))
      (T
       (PRFMAX (SUCCESSORS (RECTIFY (CAR U)))
	       (CONS ALPHA (QUOTE ALPHA-CUTOFF))
	       NIL
	       ALPHA
	       BETA)))))))
EXPR)

(DEFPROP RECTIFY
 (LAMBDA(P)
  (PROG	(Z Q)
	(SETQ Q (COMMONTAIL P P1))
   L1	(COND ((EQUAL Q P1) (GO L2)))
	(REVERT)
	(GO L1)
   L2	(SETQ Z (LISTSUBT P P1))
   L3	(COND ((NULL Z) (RETURN P)))
	(UPDATE (CAR Z))
	(SETQ Z (CDR Z))
	(GO L3)))
EXPR)

(DEFPROP COMMONTAIL
 (LAMBDA (U V) (REVERSE (COMMONHEAD (REVERSE U) (REVERSE V))))
EXPR)

(DEFPROP COMMONHEAD
 (LAMBDA(U V)
  (COND	((OR (NULL U) (NULL V) (NOT (EQUAL (CAR U) (CAR V)))) NIL)
	(T (CONS (CAR U) (COMMONHEAD (CDR U) (CDR V))))))
EXPR)